package com.googlecode.kipler.satisfiability.completion.rule.individual.uniformnotation;

import com.googlecode.kipler.syntax.LTLBinaryOperator;
import com.googlecode.kipler.syntax.LTLUnaryOperator;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.LTLBinaryConcept;
import com.googlecode.kipler.syntax.concept.LTLUnaryConcept;


public class UntilBetaConcept implements BetaConcept {

	private LTLBinaryConcept binCon;

	private Concept beta1, beta2;

	private boolean valid;

	public UntilBetaConcept() {
		super();
	}

	public UntilBetaConcept(Concept concept) {
		setBeta(concept);
	}

	@Override
	public Concept getBeta() {
		return binCon;
	}

	@Override
	public void setBeta(Concept concept) {
		valid = false;
		if (concept instanceof LTLBinaryConcept) {
			binCon = (LTLBinaryConcept) concept;
			if (binCon.getConstructor() == LTLBinaryOperator.UNTIL) {
				beta1 = binCon.getRhs();
				beta2 = new BooleanConcept(
						BooleanConcept.Constructor.INTERSECTION, binCon
								.getLhs(), new LTLUnaryConcept(
								LTLUnaryOperator.NEXT, binCon));
				valid = true;
			}
		}
	}

	@Override
	public Concept getBeta1() {
		return beta1;
	}

	@Override
	public Concept getBeta2() {
		return beta2;
	}

	public boolean isValid() {
		return valid;
	}

}
